In this paper a cyclic place-timed controlled marked graph (PTCMG), which is an extended class of a cyclic controlled marked graph (CMG), is presented as a model of discrete event systems (DESs). In a PTCMG, time constraints are attached to places instead of transitions. The time required for a marked place to be marked again is represented in terms of time constraints attached to places. The times required for an unmarked place to be marked under various controls, are calculated. The necessary and sufficient condition for a current marking to be in the admissible marking set with respect to the given forbidden condition is provided, as is the necessary and sufficient condition for a current marking to be out of the admissible marking set with respect to the forbidden condition in one transition. A maximally permissive state feedback control is synthesized in a PTCMG to guarantee a larger admissible marking set than a CMG for most forbidden state problems. Practical applications are illustrated for a railroad crossing problem and an automated guided vehicle (AGV) coordination problem in a flexible manufacturing facility.

The usage of a diagram, which we call a state fence diagram (SFD), for analyzing discrete event systems such as reactive systems, is presented. This diagram is useful for event concurrent response and scenario analysis by using its three description styles.

We study state feedback control of discrete event systems described by the Golaszewski-Ramadge model. We derive a necessary and sufficient condition for the existence of a balanced state feedback controller under partial observations.

In this paper, we discuss an abstraction method for Petri nets based on an equivalence of firing sequences of a specified subnet or a specified subset of transitions. Specifically, a method is presented to generate an equivalent net which preserves firing sequences of a specified subnet or a specified subset of transitions. The abstraction can be applied to an efficient behavioral analysis of concurrent systems constructed by composition of modules such as communication networks and Flexible Manufacturing Systems (FMS).

The symbolic model checking algorithm was proposed for the efficient verification of sequential circuits. In this paper, we show that this algorithm is applicable to the verification of concurrent systems described by finite capacity Petri nets. In this algorithm, specifications of the system are given in the form of temporal logic formulas, and the algorithm checks whether these formulas hold in the state space. All logical operations are performed on Binary Decision Diagrams. Since the algorithm does not enumerating each state, the problem of state space explosion can be avoided in many cases.

We present that event-transition diagrams are useful to analyze event concurrent response visually. Event-transition diagrams are dual for state-transition diagrams in graph theory. As an example of an usage of an event-transition diagram, a simple model of a railroad crossing is presented.

Many typical control problems such as deadlock avoidance problems and mutual exclusion problems can be formulated as forbidden marking problems. This paper studies a forbidden marking problem in controlled complementary-places Petri nets, which are suitable model for sequential control systems. We show a necessary and sufficient condition for the existence of a control law for this problem. We also obtain a maximally permissive control law which allows a maximal number of transitions to fire subject to a condition that forbidden markings will never be reached.

State space explosion is a serious problem in analyzing discrete event systems that allow concurrent occurring of events. A new method is proposed for generating reduced state spaces of systems. This method is an improvement of Valmari's stubborn set method. The generated state space preserves liveness, livelocks, and terminal states of the ordinary state space. Petri nets are used as a model of systems, and a method is shown for generating a reduced state space from a given Petri net.

Net theory originated by Dr. Petri in 1962 is now indispensable key concept in the analysis and design of concurrent systems. In Japan, since late seventies the net theory has attracted attention among computer scientists. This paper reviews the historical aspect of the net theory developed in Japan during the last two decades.

This paper describes MENDELS ZONE, a Petri-net-based concurrent programming environment, which is especially suitable for cooperating discrete event systems. MENDELS ZONE adopts MENDEL net, which is a type of high level (hierarchical colored) Petri net. One of the characteristics of the MENDEL nets is a process-oriented hierarchy like CCS, which is different from the subnet-oriented hierarchy in the Jensen's hierarchical colored Petri net. In a process-oriented hierarchy, a hierarchical unit is a process, which is more natural for cooperating and decentralized discrete event control systems. This paper also proposes a design methodology for MENDEL nets. Although many Petri net tools have been proposed, most tools support only drawing, simulation, and analysis of Petri nets; few tools support the design methodology for Petri nets. While Petri nets are good final design documents easy to understand, analyzable, and executable it is often difficult to write Petri nets directly in an earlier design phase when the system structure is obscure. A proposed design methodology makes a designer to construct MENDEL nets systematically using causality matrices and temporal logic. Furthemore, constructed MENDEL nets can be automatically compiled into a concurrent programming language and executed on a parallel computer.

A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.